Tamarin Models

Below is a brief summary of the formal models used in our paper, done using the Tamarin Prover.

Mobile Visa Model – Formal model for Visa transactions done via payment apps, in normal as well as transport mode (both Apple Pay, Samsung Pay are modelled).

Mobile Mastercard Model – Formal model for Mastercard transactions done via payment apps, in normal as well as transport mode (both Apple Pay, Samsung Pay are modelled).

Modified Basin Visa Model – An updated model for Visa transactions done via a (plastic) card, with more details around the [IAD] and its checks; it proves that checking the format of the IAD for Visa cards would in fact detect a previous contactless limit bypass attack proposed in The EMV Standard: Break, Fix, Verify.

L1RP Model – Formal model proving the security of our new proposed protocol, L1RP.